=============================
Step 1

? (all x ((inv (inv x)) = x))


> revsk
=============================
Step 2

? ((inv (inv c23546)) = c23546)


> hypdisj
=============================
Step 3

? ((inv (inv c23546)) = c23546)


> rewriteB (inv (inv c23546))
|=============================
|Step 4
|
|? ((+ e (inv (inv c23546))) = (inv (inv c23546)))
|
|
|> (((+ e X) = X) <--)
=============================
Step 5

? ((+ e (inv (inv c23546))) = c23546)


> rewriteB e
|=============================
|Step 6
|
|? ((+ Var77 (inv Var77)) = e)
|
|
|> (((+ X (inv X)) = e) <--)
=============================
Step 7

? ((+ (+ c23546 (inv c23546)) (inv (inv c23546))) = c23546)


> rewriteB (+ (+ c23546 (inv c23546)) (inv (inv c23546)))
|=============================
|Step 8
|
|? ((+ c23546 (+ (inv c23546) (inv (inv c23546)))) = (+ (+ c23546 (inv c23546)) (inv (inv c23546))))
|
|
|> (((+ X (+ Y Z)) = (+ (+ X Y) Z)) <--)
=============================
Step 9

? ((+ c23546 (+ (inv c23546) (inv (inv c23546)))) = c23546)


> rewriteA (+ (inv c23546) (inv (inv c23546)))
|=============================
|Step 10
|
|? ((+ (inv c23546) (inv (inv c23546))) = e)
|
|
|> (((+ X (inv X)) = e) <--)
=============================
Step 11

? ((+ c23546 e) = c23546)


> (((+ X e) = X) <--)

=============================
Step 1

? (all x ((+ (inv x) x) = e))


> revsk
=============================
Step 2

? ((+ (inv c23099) c23099) = e)


> hypdisj
=============================
Step 3

? ((+ (inv c23099) c23099) = e)


> rewriteB c23099
|=============================
|Step 4
|
|? ((inv (inv c23099)) = c23099)
|
|
|> (((inv (inv X)) = X) <--)
=============================
Step 5

? ((+ (inv c23099) (inv (inv c23099))) = e)


> (((+ X (inv X)) = e) <--)
